es:ES, ff:FIFO, i:ff.C, e, e':{e:E| ff.R(i,e)} , j:ff.C.
(ff.S(j,i,ff.Sender(i,e)))
 (ff.S(j,i,ff.Sender(i,e')))
 (ff.Sender(i,e) = ff.Sender(i,e')  E)
 (e = e') 

latex

Definitions	x:A. B(x), FIFO, P  Q, t  T, , x:A. B(x), e c e', P  Q, False
Lemmas	es-E wf, fifoSender wf, fifoC wf, fifoS wf, fifoR wf, es-state wf, es-loc wf, fifo wf, event system wf, fifoSender-preserves-order, es-le-causle, es-le weakening eq, es-causl transitivity2, es-causl irreflexivity